#!/usr/bin/awk -f
{
if( /<!-- #include virtual=.* -->/ ) {
  split($0,A,"\"");
  filename = "." A[2];
  while(getline < filename) {
      print;
  }
}  
else {
    print;
}
  
}
